[レポート] SEC301 データプライバシーとセキュリティ担保の裏にある理論と数学 #reinvent

re:Invent 2018のセッションSEC301: "The Theory and Math Behind Data Privacy and Security Assurance"についてのレポートです。

公式ページのセッション概要を引用します。

Data privacy and security are top concerns for customers in the cloud. In this session, the AWS Automated Reasoning group shares the advanced technologies, rooted in mathematical proof, that help provide the highest levels of security assurance in today's data-driven world. The Automated Reasoning group co-presents with Bridgewater, a customer that has leveraged these technologies to help confirm that security requirements are being met, an assurance not previously available from conventional tools.

セッションメモ

• 次世代のセキュリティ技術＝(数学的意味での)証明可能なセキュリティ
• 共有責任モデルに「証明可能なセキュリティ」を追加します

  

• Zelkovaとは？

  • クラウドのカスタマーに対して証明可能なセキュリティを
  • IAMについての自動推論を強化することによって
  • エンタープライズガバナンスとデータプライバシーの制御をスケールする形で提供
• Zelkovaが依拠するのは数学と論理。それらによりデータプライバシーを担保している

• 例：S3バケットポリシー
  • ポリシーの要素は、論理記号とみなせる

• Zelkobaは、論理ソルバーが解釈できるようポリシーを変換、結果をJSONで返す

• IAMポリシーを論理式にエンコード

• 統合による自動化
  • AWS Configと連携し、ポリシーの変更からSNSによる通知を受けて、lambdaでZelkovaが実行、検証を行われる

• Bridgewaterアソシエイツの事例紹介
  • 世界最大のヘッジファンド
  • たくさんのAWSアカウントを使用して、世界経済や市場の分析をシステム化している

• BridgewaterはZelkovaを以下のような目的で活用している
  • データを不用意に公開してしまうような設定ミスの発見
  • 変更が必要なポリシー宣言の識別
  • 弱点解消のための計画された変更内容のチェック
  • 所有する全アカウントにわたるポリシー監査
• Zelkovaをどう使っているか
  • ポリシーの変更を検出する
  • 損害が生じる前に不良を検出
• Zelkovaをどう使っているか2
  • ポリシーを適用する前に、CI/CDプロセスの一環として検証を行う
  • 損害が発生しうる可能性が生じる前に不良を検出

• ポリシーに対するZelkovaの呼び出し例

• Zelkovaのまとめ
  • 形式的で正確
  • 一貫性がある
  • IAMポリシーの意味を十分に理解している(呪文ではない)
• さらに知りたい場合は
  • クローズドベータに参加
  • アカウントマネージャもしくはTAMにお気軽に依頼
  • BWやベータコミュニティが開発したユースケース
  • 発表者(Nehaさん)にブースで聞いてください

感想

Zelkovaについて聞いたのは初めてでしたが、証明可能なセキュリティという概念はとても面白いと感じました。IAMポリシーや、その組み合わせの本質は(数学や論理学の意味での)論理式と捉えることができて、それは制約検証が可能だ、というのはたしかに面白い視点だと思います。国際会議(学会)での発表もされているということでした。